;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "Mvolume.lisp")
;(require "Mvolatility.lisp")
(require "Mstock-retrieval.lisp")
;(require "Mperformance.lisp")
;(require "Mio.lisp")
;(require "Mhelpers.lisp")
(require "M-avl-string-keys.lisp")

(module Tvolume
  (import Ivolume)
  (import Itree)
  
; check-expect tests  
  (include-book "list-utilities" :dir :teachpacks)
  (include-book "io-utilities" :dir :teachpacks)
  (include-book "testing" :dir :teachpacks)
  (check-expect (volume "XYZCorp" nil 0) "XYZCorp: 0 ")
  (check-expect (volume "XYZCorp" nil 37) "XYZCorp: 37 ")
  (check-expect (volume "XYZCorp" 
                        (list '("XYZCorp" 30.12 34.23 35.66 36.35 1050)
                              '("ABCCorp" 35.43 39.33 38.55 37.79 1200)
                              '("MNOCorp" 37.99 41.53 42.88 41.55 1500)
                              '("ABCCorp" 33.77 38.43 37.95 37.88 1100)
                              '("XYZCorp" 37.22 36.22 37.31 36.89 1200)
                              '("MNOCorp" 39.01 42.53 43.11 42.93 1550)) 0) 
                "XYZCorp: 2250 ")
  (check-expect (volume "DEFCorp" 
                        (list '("XYZCorp" 30.12 34.23 35.66 36.35 1050)
                              '("ABCCorp" 35.43 39.33 38.55 37.79 1200)
                              '("MNOCorp" 37.99 41.53 42.88 41.55 1500)
                              '("ABCCorp" 33.77 38.43 37.95 37.88 1100)
                              '("XYZCorp" 37.22 36.22 37.31 36.89 1200)
                              '("MNOCorp" 39.01 42.53 43.11 42.93 1550)) 0) 
                "DEFCorp: 0 ")

  ;property definitions
  (include-book "doublecheck" :dir :teachpacks) 
  ; random stock-list generator for property definitions
  ; tests that the volume function always returns a string
  ; random date
  (defrandom random-date ()
    (int->str (random-between 19000101 20990101)))
  
  ; random stock entry from the file, includes the date
  (defrandom random-stocks-file-line ()
    (list (random-date) (random-string) (random-natural) (random-natural)
          (random-natural) (random-natural) (random-natural)))
  
  ; random stock entry from within the sub-trees in the AVL tree
  (defrandom random-stock-entry ()
   (list (random-string) (random-natural) (random-natural)
         (random-natural) (random-natural) (random-natural)))
                                                             
  
  ; random tree - constructs an AVL tree
  ; given a list of stock file lines
  ; using insert-record
  (defun generate-tree (stocks tree)
    (if (consp stocks)
        (let* ((stock (car stocks))
           (date (car stock))
           (ticker (cadr stock))
           (opening-price (caddr stock))
           (highest-price (cadddr stock))
           (lowest-price (car (cddddr stock)))
           (closing-price (car (cdr (cddddr stock))))
           (num-traded (car (cdr (cdr (cddddr stock)))))
           (datalist (list opening-price highest-price lowest-price closing-price num-traded)))
      (if (equal (avl-retrieve tree date) nil)
          (generate-tree (cdr stocks) (avl-insert tree date (avl-insert (empty-tree) ticker datalist))) ; if the given date doesn't exist, create it in the tree
          (generate-tree (cdr stocks) (avl-insert tree date (avl-insert (cdr (avl-retrieve tree date)) ticker datalist)))))
        tree))
  
  ; random tree
  (defrandom random-stock-tree ()
    (generate-tree (random-list-of (random-stocks-file-line)) (empty-tree)))

  (defproperty volume-returns-string-prp
    (ticker :value (random-string) 
     data   :value (random-list-of (list (random-string) (random-rational) (random-rational)
                                         (random-rational) (random-rational) (random-natural)))
     count  :value (random-natural))
    (equal t (stringp (volume ticker data count))))
  ; tests that the volume function always returns a string consisting of a ticker and a natural
  (defproperty volume-returns-ticker-and-natural-prp
    (ticker :value (random-string) 
            :where (consp (str->chrs ticker))
     data   :value (random-list-of (list (random-string) (random-rational) (random-rational)
                                         (random-rational) (random-rational) (random-natural)))
     count  :value (random-natural))
    (equal t (and (= (len (words (volume ticker data count))) 2)
                  (> (len (str->chrs (car (words (volume ticker data count))))) 1)
                  (natp (str->int (cadr (words (volume ticker data count))))))))
  ; tests that the volume-query function always returns a string
  (defproperty volume-query-returns-string-prp
    (start   :value (random-date)
     end     :value (random-date)
             :where (<= (str->int end) (str->int start))
     tickers :value (random-list-of (random-string))
     tree    :value (random-stock-tree))
    (equal t (stringp (volume-query start end tickers tree))))
  )

(link RTvolume (Mtree Mstockretrieval Mvolume Tvolume))
(invoke RTvolume)
  
